E, X1, X2:Type, dE:EqDecider(E), dL:EqDecider(IdLnk), info:(E(IdX1+(IdLnkE)X2)), e, r:E,
l:IdLnk.
rcv-from-on(dE;dL;info;e;l;r)  rcv?(r) & sender(r) = e & link(r) = l 

latex

Definitions	rcv?(e), Id, EqDecider(T), rcv-from-on(dE;dL;info;e;l;r), Unit, b, A, , p  q, eqof(d), True, b, P  Q, P  Q, Prop, P & Q, sender(e), IdLnk, link(e), x:A. B(x), P  Q, t  T, A & B, False
Lemmas	link wf, sender wf, false wf, true wf, eqof wf, band wf, assert wf, bool wf, rcv? wf, not wf, bnot wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, deq wf, IdLnk wf, Id wf, deq property, and functionality wrt iff, iff functionality wrt iff, assert of band